Agda and Lean: functional programming meets proving

Some programming languages, like Agda, Coq, and Lean, go beyond transforming inputs to outputs by also formalizing logical reasoning and verifying code correctness. They use a functional style with constructors, recursion, and pattern matching, but also include a dependent type system, which adds this extra expressiveness. Using Agda and Lean, we will learn all these concepts, both from a theoretical and practical point of view. All this through many examples such as demonstrating arithmetic properties or analyzing the complexity of sorting algorithms.

What attendees will learn

This workshop has two objectives:

• To understand the basis on which formal verification languages like Agda and Lean are built: a functional language with dependent types that allows the construction of new objects and propositions. We will work with many examples to see how naturally the functional paradigm and logical reasoning fit together.
• To get to know the Agda and Lean programming languages and the universe that surrounds them. We will develop with them our own functionalities, and at the same time we will learn how to work with them, the evolution they have had, the available resources and the impact they have today.

Requirements for the workshop

• Computer with Agda & Lean installed (guide / sources / slides / repo to be published)
• Basic knowledge of functional programming

Agenda/Plan for the workshop

Intro

Part I - Agda

The Basics - From Haskell to Agda
In a nutshell - Dependent types
Hands on - Arithmetic & Propositions

Break

Part II - Lean

The Basics - From proofs to programs
In a nutshell - Logic & the Curry-Howard correspondence
Hands on - Tactics
All in practice: Sorting algorithms
Outro

Target audience roles

Software engineers